<table width="572" border="0">
    <tr>
      <td width="277"><a href="#a">程序设计语言及其实现技术&nbsp;</td>
      <td width="279"><a href="#b">并发程序形式语义及其应用&nbsp;</td>
    </tr>
    <tr>
      <td height="33"><a href="#c">语义网及本体工程&nbsp;</td>
      <td><a href="#d">形式化方法及其在软件开发中的应用&nbsp;</td>
    </tr>
  </table>
  <p>
  </p>
  <table width="568" height="524" border="0">
    <tr>
      <td width="556" height="35" align="center"><span class="STYLE1"><span class="STYLE2"><a name="a">程序设计语言及其实现技术&nbsp;</span></td>
    </tr>
    <tr>
      <td height="242" align="left" valign="top"><p>研究各种程序设计语言以及它们的设计、分析和实现技术。在这方面的研究主要包括：</p>
        <ul>
          <li>同种类的通用程序设计语言，包括过程式程序设计语言、函数式程序设计语言、逻辑式程序设计语言、面向对象语言和并行程序设计语言等的形式语法、形式语义和类型理论等；</li>
          <li> 各种程序设计语言的实现技术，尤其是编译程序的设计方法和实现技术；近年来还研究专用语言的实现技术，如面向符号和自动测试的语言ATLAS的编译器的设计与实现；</li>
          <li> 各种程序分析技术，如静态和动态分析、数据流分析、控制流分析、概念分析、程序分片和部分求值技术等；</li>
          <li> 程序转换技术；</li>
        </ul>
        &nbsp;</td>
    </tr>
    <tr>
      <td align="center" valign="top"><span class="STYLE2"><a name="b">并发程序形式语义及其应用&nbsp;</span></td>
    </tr>
    <tr>
      <td><p>　　研究并发形式化模型及其应用，并发程序的形式化方法。尤其是研究Monad理论及其在软件开发方面的应用；研究Action演算、Seal演算和Ambient演算等描述并发或（和）移动的形式化描述模型的性质和描述能力，以及对分布式系统、并发交互系统的形式化描述和对这些系统进行安全性、移动性和可靠性等性能的分析。</p>
        <p>　　在这方面已经有四位博士完成了相关领域的博士论文。</p>&nbsp;</td>
    </tr>
    <tr>
      <td align="center" valign="top"><span class="STYLE2"><a name="c">语义网及本体工程</span></td>
    </tr>
    <tr>
      <td valign="top"><p>　　语义万维网（Semantic Web，简称语义网）是计算机信息处理领域当前研究的热点之一，其基本思想是对当前的万维网进行扩展，使得网络中所有信息都是具有语义的，是计算机能够理解和处理的，便于人和计算机之间的交互与合作。</p>
        <p>　　本体（Ontology）是某一领域共享概念模型的明确表示和描述，是语义研究的热点，是语义网实现的基础和关键。本体工程关注于本体的建立和使用，其研究内容主要包括本体的学习、建造、演化、映射、合并和评价等，其研究成果对语义网的发展具有重要的推动作用。</p>
        <p>　　本实验室的语义网研究项目组正在本体工程领域、语义网领域和面向服务的计算等领域进行深入的研究。主要研究内容包括本体建模、本体映射、本体演化、智能搜索、信息提取、智能信息系统、语义网服务等。        </p>
        &nbsp;</td>
    </tr>
    <tr>
      <td align="center" valign="top"><span class="STYLE2"><a name="d">形式化方法及其在软件开发中的应用&nbsp;</span></td>
    </tr>
    <tr>
      <td><p>　　形式化方法是指以数学模型为基础对软件和硬件系统进行对规范化描述，并应用于软件的开发和验证等方面的技术。形式化的软件开发，就是用形式化的语言来描述软件需求和特征，并且通过推理验证来保证最终的软件产品是否满足这些需求和具备这些特征。形式化方法尤其是在研究高集成系统中非常有用，特别是在研究这些系统的可靠性和安全性等方面。形式化方法还能帮助发现其它方法不容易发现的系统描述的不一致，不明确或不完整，有助于增加软件开发人员对系统的理解，因此采用形式化软件开发方法可以有效地提高软件质量。</p>
        <p> 　　研究形式化方法以及在软件开发的各个过程中的应用主要包括：</p>
        <ul>
          <li>研究各种形式化描述语言并设计实现形式化模型；</li>
          <li>研究各种形式化规范方法和技术， 以及在软件测试和软件检查中如何应用形式化规范；</li>
          <li> 并发程序的形式化描述、测试和验证等；<br>
          </li>
        </ul>&nbsp;</td>
    </tr>
  </table>